Simplify liveness proof of zookeeper controller #166

euclidgame · 2023-07-04T21:10:26Z

In this PR, I mainly do two things:

Some straightforward simplifications for liveness proof of zookeeper controller.
Apply some lemmas (properties) of zookeeper controller to all controllers.

marshtompsxd · 2023-07-05T06:20:43Z

src/controller_examples/zookeeper_controller/proof/common.rs

-        &&& s.reconcile_state_of(zk.object_ref()).pending_req_msg.is_Some()
-        &&& s.message_in_flight(s.pending_req_of(zk.object_ref()))
-        &&& is_create_stateful_set_request_msg(s.pending_req_of(zk.object_ref()), zk)
+pub open spec fn is_correct_pending_request_at_zookeeper_step(


marshtompsxd · 2023-07-05T06:25:29Z

src/controller_examples/zookeeper_controller/proof/liveness.rs

        lift_state(current_state_matches(zk)),
        always(lift_state(current_state_matches(zk)))
    );
 }

+proof fn lemma_from_pending_req_in_flight_at_some_step_to_next_step(


This is nice!

I am even thinking about whether we can further generalize this lemma (make it applicable to all controllers), but let's leave it for future PRs

Could you document this lemma? Especially why we need these preconditions. The documentation will help us later a lot.

I am even thinking about whether we can further generalize this lemma

This is what we need to do later.

And generalizing it seems not difficult but requires more handlings of "correct requests".

marshtompsxd · 2023-07-05T06:30:11Z

src/controller_examples/zookeeper_controller/proof/liveness.rs

-
-proof fn lemma_from_after_create_client_service_step_to_after_create_admin_server_service_step(
-    spec: TempPred<ClusterState>, zk: ZookeeperClusterView, resp_msg: Message
+proof fn lemma_from_resp_in_flight_at_some_step_to_pending_req_at_next_step(


Similarly, could you document this lemma?

marshtompsxd · 2023-07-05T06:31:06Z

src/controller_examples/zookeeper_controller/proof/liveness.rs

-            &&& s_prime.message_in_flight(resp_msg)
-            &&& resp_msg_matches_req_msg(resp_msg, req_msg)
-        });
+    assert forall |s, s_prime| pre(s) && #[trigger] stronger_next(s, s_prime) implies pre(s_prime) || post(s_prime) by {


Is this for proof stability?

Yes, it is.

marshtompsxd · 2023-07-05T06:38:13Z

src/controller_examples/zookeeper_controller/proof/liveness.rs

+        step != ZookeeperReconcileStep::Error, step != ZookeeperReconcileStep::Done,
+        next_step != ZookeeperReconcileStep::Init,
+        forall |zk_1: ZookeeperClusterView, resp_o: Option<APIResponse>|
+            #[trigger] reconcile_core(zk_1, resp_o, ZookeeperReconcileState{ reconcile_step: step }).0.reconcile_step == next_step


I think this precondition wants to say no matter what, the next step is next_step. I am trying to understand why we have to forall zk_1 here, instead of just talking about zk.

We can't infer from the pre state that the cr passed to reconcile_core is exactly zk. However, we may weaken the precondition for this lemma.

Signed-off-by: Wenjie Ma <[email protected]>

marshtompsxd · 2023-07-05T17:48:38Z

src/kubernetes_cluster/proof/controller_runtime_safety.rs

+// The proof is very straightforward:
+//   - Right after the controller enters 'state', the pending request is added to in_flight.
+//   - If the pending request is processed by kubernetes api, there will be a response in flight.
+//   - If the response is processed by the controller, the controller will either enter a new state or a new pending request in flight.


either enter a new state or a new pending request in flight

Or?

Yes. By this I mean the controller will not necessarily enter a new state; if it enters a state that is same as 'state', then a new pending request will be in flight, so in this case the invariant will not be violated.

I see what you mean. Maybe it is better to say "If the response is processed by the controller, the controller will either the next state (which could still be 'state' but the invariant still holds then)."

Signed-off-by: Wenjie Ma <[email protected]>

marshtompsxd · 2023-07-05T18:12:19Z

src/controller_examples/zookeeper_controller/proof/common.rs

        &&& s.reconcile_state_of(zk.object_ref()).pending_req_msg.is_Some()
-        &&& is_create_config_map_request_msg(s.pending_req_of(zk.object_ref()), zk)
+        &&& is_correct_pending_request_msg_at_zookeeper_step(step, s.pending_req_of(zk.object_ref()), zk, object)
        &&& s.message_in_flight(resp_msg)
        &&& resp_msg_matches_req_msg(resp_msg, s.pending_req_of(zk.object_ref()))
    }
 }


I think the above spec functions can be made more generic and will be reused heavily. But to do so we might need to make the step an associated type of Reconciler and the spec functions need to take a closure for is_correct_pending_request_msg_at_zookeeper_step. We can work on this later.

Absolutely.

take a closure for is_correct_pending_request_msg_at_zookeeper_step

Actually I have more thoughts about this... I will put it in the issue.

marshtompsxd · 2023-07-05T18:17:16Z

src/controller_examples/zookeeper_controller/proof/liveness.rs

        lift_state(current_state_matches(zk)),
        always(lift_state(current_state_matches(zk)))
    );
 }

+// This lemma ensures that zookeeper controller at some step with pending request in flight will finally enter its next step.


To avoid ambiguity, you can say "This lemma ensures that zookeeper controller at step a with pending request in flight will finally enter step b." and use step a, step b below, instead of initial, final step. My first reaction when seeing initial step is actually ZookeeperReconcileStep::Init

marshtompsxd · 2023-07-05T18:18:28Z

src/controller_examples/zookeeper_controller/proof/liveness.rs

+// For the initial state and final state, they both require the reconcile_state to have a pending request which is the correct
+// request for that step (parameter 'step' for the initial step, parameter 'next_step' for the final state).
+// Note that in this lemma we add some constraints to the initial step:
+//    1. The next step of it when conducting reconcile_core is deterministic.


Instead of deterministic, I think what you mean is that there is only one possible next step (i.e., step b) for step a. The reconcile_core is still deterministic even with branches.

marshtompsxd · 2023-07-05T18:21:03Z

src/controller_examples/zookeeper_controller/proof/liveness.rs

+// request for that step (parameter 'step' for the initial step, parameter 'next_step' for the final state).
+// Note that in this lemma we add some constraints to the initial step:
+//    1. The next step of it when conducting reconcile_core is deterministic.
+//    2. When the controller enters this step, it must creates a request (which will be used to create the pending request message)


"which will be used to create the pending request message" --> "which is piggybacked by the pending request message"

Typo: creates -> create

marshtompsxd · 2023-07-05T18:22:48Z

src/controller_examples/zookeeper_controller/proof/liveness.rs

-proof fn lemma_from_after_create_headless_service_step_to_after_create_client_service_step(
-    spec: TempPred<ClusterState>, zk: ZookeeperClusterView, resp_msg: Message
+// This lemma ensures that zookeeper controller at some step with a response in flight that matches its pending request will finally enter its next step.
+// For the initial state and final state, they both require the reconcile_state to have a pending request which is the correct


Similar comment as above. Try to avoid using initial and final here

marshtompsxd · 2023-07-05T18:24:05Z

src/controller_examples/zookeeper_controller/proof/liveness.rs

+// request for that step (parameter 'step' for the initial step, parameter 'result_step' for the final state). For the initial state
+// alone, there is a known response (the parameter resp_msg) in flight that matches the pending request.
+// Note that in this lemma we add some constraints to the initial step:
+//    1. The next step of it when conducting reconcile_core is deterministic.


Similar comment for "deterministic"

marshtompsxd · 2023-07-05T18:25:33Z

src/controller_examples/zookeeper_controller/proof/liveness.rs

+// alone, there is a known response (the parameter resp_msg) in flight that matches the pending request.
+// Note that in this lemma we add some constraints to the initial step:
+//    1. The next step of it when conducting reconcile_core is deterministic.
+//    2. When the controller enters this step, it must creates a request (which will be used to create the pending request message)


Similar comment

Signed-off-by: Wenjie Ma <[email protected]>

euclidgame changed the title ~~Simplify liveness proof~~ Simplify liveness proof of zookeeper controller Jul 4, 2023

marshtompsxd reviewed Jul 5, 2023

View reviewed changes

euclidgame added 7 commits July 5, 2023 11:16

Remove redundant preconditions in controller_runtime_liveness

97e53f9

Signed-off-by: Wenjie Ma <[email protected]>

Use at_zookeeper_step_with_zk

590b375

Signed-off-by: Wenjie Ma <[email protected]>

Unify specs for different steps of zookeeper controller

39ceda8

Signed-off-by: Wenjie Ma <[email protected]>

Simplify rules for pending_req /\ step ~> pending_req /\ next_step

7eed933

Signed-off-by: Wenjie Ma <[email protected]>

Add one assertion to make the proof go through

4e5ec9a

Signed-off-by: Wenjie Ma <[email protected]>

Lift some of zookeeper liveness property to all controllers

9defffd

Signed-off-by: Wenjie Ma <[email protected]>

Fix all the lemmas after supporting kubernetes is busy

3b3c165

Signed-off-by: Wenjie Ma <[email protected]>

euclidgame force-pushed the simplify_liveness_proof branch from 01c54de to 3b3c165 Compare July 5, 2023 16:33

euclidgame added 2 commits July 5, 2023 12:18

Add comments for the liveness lemmas

61612f8

Signed-off-by: Wenjie Ma <[email protected]>

Add comments for controller_runtime_safety lemmas

9f8d192

Signed-off-by: Wenjie Ma <[email protected]>

euclidgame requested a review from marshtompsxd July 5, 2023 17:31

marshtompsxd reviewed Jul 5, 2023

View reviewed changes

Reword some comments

abe45c3

Signed-off-by: Wenjie Ma <[email protected]>

marshtompsxd reviewed Jul 5, 2023

View reviewed changes

euclidgame requested a review from marshtompsxd July 5, 2023 18:12

marshtompsxd reviewed Jul 5, 2023

View reviewed changes

Reword some comments

53229c4

Signed-off-by: Wenjie Ma <[email protected]>

marshtompsxd merged commit 6438c35 into main Jul 5, 2023
1 check passed

marshtompsxd mentioned this pull request Jul 6, 2023

Reason about common behavior among controllers in the reconciliation logic #168

Closed

marshtompsxd deleted the simplify_liveness_proof branch August 1, 2023 21:53

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Simplify liveness proof of zookeeper controller #166

Simplify liveness proof of zookeeper controller #166

euclidgame commented Jul 4, 2023

marshtompsxd Jul 5, 2023

marshtompsxd Jul 5, 2023

marshtompsxd Jul 5, 2023

marshtompsxd Jul 5, 2023

euclidgame Jul 5, 2023

euclidgame Jul 5, 2023

marshtompsxd Jul 5, 2023

marshtompsxd Jul 5, 2023

euclidgame Jul 5, 2023

marshtompsxd Jul 5, 2023

euclidgame Jul 5, 2023

marshtompsxd Jul 5, 2023

euclidgame Jul 5, 2023

marshtompsxd Jul 5, 2023

marshtompsxd Jul 5, 2023

euclidgame Jul 5, 2023

euclidgame Jul 5, 2023

marshtompsxd Jul 5, 2023

marshtompsxd Jul 5, 2023

marshtompsxd Jul 5, 2023

marshtompsxd Jul 5, 2023

marshtompsxd Jul 5, 2023

marshtompsxd Jul 5, 2023

Simplify liveness proof of zookeeper controller #166

Simplify liveness proof of zookeeper controller #166

Conversation

euclidgame commented Jul 4, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment